es:ES, e1:E, e2:{e:E| loc(e) = loc(e1)  Id} , p, q, p',
q':({e:E| loc(e) = loc(e1)  Id} {e:E| loc(e) = loc(e1)  Id} ).
(a, b:{e:E| loc(e) = loc(e1)  Id} . (a  [e1, e2])  (b  [e1, e2])  {p(a,b)  p'(a,b)})
 (a, b:{e:E| loc(e) = loc(e1)  Id} . (a  [e1, e2])  (b  [e1, e2])  {q(a,b)  q'(a,b)})
 {[e1;e2]~([a,b].p(a,b))*[a,b].q(a,b)  [e1;e2]~([a,b].p'(a,b))*[a,b].q'(a,b)} 

latex

Definitions	x:A. B(x), Id, , P  Q, {T}, x(s1,s2), [e1;e2]~([a,b].p(a;b))*[a,b].q(a;b), t  T, x:A. B(x), {i..j}, P & Q, i  j < k, A  B, A, False, P  Q, P  Q, T, True, A c B, x,y. t(x;y), S  T, suptype(S; T),
Lemmas	es-pstar-q wf, le wf, es-locl-iff, es-pred wf, es-le-loc, es-loc wf, es-loc-pred, Id wf, int seg wf, es-le wf, es-locl wf, squash wf, true wf, es-E wf, l member wf, es-interval wf, event system wf, es-increasing-sequence2, member-es-interval, es-le transitivity, es-le weakening eq, es-le-pred, es-locl transitivity1, es-pred-locl, es-locl transitivity2, es-le weakening